M1, M2:MsgA, k:Knd. M1  M2  (M2.da(k) r M1.da(k)) 

latex

Definitions	x:A. B(x), P  Q, M.da(a), t.1, t.2, t  T, MsgA, M1  M2, Valtype(da;k), A c B, P & Q,
Lemmas	subtype-fpf-cap-top, top wf, Knd wf, Kind-deq wf, ma-sub wf, msga wf